Renaming proverArgs annotation and cleaning up annotation handling#932
Merged
Conversation
…nabled proverConfigArgs annotation for functions
There was a problem hiding this comment.
Pull Request Overview
This PR renames the proverArgs annotation to proverConfigArgs, centralizes annotation handling in a new AnnotationSupporter, and extends proverConfigArgs support to function verification.
- Renamed and unified annotation parsing for prover configuration flags
- Refactored exhale, join, and state consolidation annotation logic into
AnnotationSupporter - Enabled and reset prover configuration options in function verification units
Reviewed Changes
Copilot reviewed 8 out of 8 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| src/main/scala/verifier/DefaultMainVerifier.scala | Switched to AnnotationSupporter for exhale and join mode annotations; updated proverConfigArgs printing |
| src/main/scala/verifier/BaseVerifier.scala | Replaced inline stateConsolidationMode parsing with AnnotationSupporter call |
| src/main/scala/supporters/functions/FunctionVerificationUnit.scala | Added function-level proverConfigArgs support and reset logic |
| src/main/scala/supporters/MethodSupporter.scala | Replaced ad-hoc proverArgs parsing with AnnotationSupporter.getProverConfigArgs |
| src/main/scala/supporters/AnnotationSupporter.scala | New helper for all annotation parsing and warning reporting |
| src/main/scala/rules/ExecutionFlowController.scala | Replaced inline exhaleMode parsing with AnnotationSupporter.getExhaleMode |
| src/main/scala/rules/Brancher.scala | Renamed brancher variables from proverArgs to proverConfigArgs |
| silver | Updated submodule commit |
Comments suppressed due to low confidence (3)
src/main/scala/supporters/AnnotationSupporter.scala:22
- [nitpick] Add Scaladoc comments to this method (and the others in AnnotationSupporter) to explain its purpose, parameters, return value, and side effects (warnings).
def getProverConfigArgs(member: ast.Member, reporter: Reporter): Map[String, String] = {
src/main/scala/verifier/DefaultMainVerifier.scala:324
- [nitpick] The variable name
mceis not immediately clear to readers. Consider renaming to something likemoreCompleteExhaleEnabledorshouldUseMoreCompleteExhalefor clarity.
val mce = AnnotationSupporter.getExhaleMode(member, reporter) match {
src/main/scala/supporters/functions/FunctionVerificationUnit.scala:153
- New handling of
@proverConfigArgsfor functions is introduced here; consider adding unit or integration tests to verify that function-level annotations are correctly parsed and applied.
val proverOptions: Map[String, String] = AnnotationSupporter.getProverConfigArgs(function, reporter)
This was referenced Jun 24, 2025
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR
proverArgs, (i.e. for example@proverArgs("smt.arith.solver=6")) toproverConfigArgs(i.e. for example@proverConfigArgs("smt.arith.solver=6")). This change makes the annotation's name consistent with the corresponding command line option--proverConfigArgs, which serves the same function, and fixes an accidental name clash with the--proverArgscommand line option which also exists but does something different (it passes command line options to Z3).proverConfigArgsannotation also for function verification (it previously only worked for methods)AnnotationSupporter.These changes address two problems raised in issue #931.